FDL - Step of Proof: mu'

Step of Proof: mu'_wf

11,40

Inference at * 1
Iof proof for Lemma mu' wf:

.....equality..... NILNIL

1. A : Type
2. P : A

x:A. Dec(

. (

(P(x,n))))

TERMOF{p-mu-decider:ObjectId, 1:l, 1:l} ~ TERMOF{p-mu-decider:ObjectId, 1:l, i:l}

by (RW (SubC (ComputeToC []) ) 0)

CollapseTHEN (Trivial)